Rsframe(${\it lnk}$; ${\it tag}$; $L$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr inr inr inr (inl $<$${\it lnk}$, ${\it tag}$, $L$$>$ )